$\forall$$T$, $A$:Type, $P$:($A$$\rightarrow$$T$$\rightarrow\mathbb{B}$), $i$:Id, $k$:Knd, $a$, $x$:Id, ${\it es}$:ES.
\\[0ex]@$i$ $k$(v:$T$) triggers local action $a$ when $P$ ($x$:$A$) v $\in$ $\mathbb{P}$